g:IMonoid. Assoc(|g|;*) & Ident(|g|;*;e) 

latex

Up	groups 1
Definitions of Statement	IsMonoid(T;op;id), IMonoid
Definitions	t  T, x:A. B(x), P & Q, IMonoid, IsMonoid(T;op;id)
Lemmas	imon wf, imon properties